Notes (Week 4 Wednesday)
These are the notes I wrote during the lecture.
We've done:
Well-formed formulas (the *syntax* of logic)
They give you rules for how to build formulas.
e.g. if you have a formula ϕ,
and a formlula ψ
then you can build a formula (ϕ ∧ ψ)
from those.
But: formally, these are just blobs of syntax
(they denote trees)
∧
/ \
/ \
ϕ ψ
...but they don't really say what the formulas mean.
We've also done Boolean algebra:
...which tells you how to calculate with:
truth values,
and machine words,
and sets,
using the same general framework
Boolean algebras give you calculation
with truth values,
&& "and" in the boolean algebra of truth values
true && false *equals* true
true && false = true
just as 1+0=1 (it's just calculation, but with truth values)
wffs give you logical expressions.
∧ "conjunction" in the boolean algebra of truth values
Doesn't calculate, it just builds formulas.
⊤ ∧ ⊥ ≠ ⊤ (because they denote different
syntax trees)
With *valuations*, we build a bridge between
our syntax (the wffs),
and boolean algebras
We define the meaning of wffs in terms of 𝔹
(the two-element boolean algebra with {true,false})
Q: Why so pedantic?
A: We want to be careful about how we build our logic,
because we want to be able to argue *formally*
that we built it right.
In particular:
we'll define what "truth" means for our wffs,
separately from how we define "proof",
to convince ourselves that our proof rules work.
a ∧ b <-- inherently neither true nor false,
it's just a piece of syntax
But I can define its *valuation* in an environment v.
⟦ ⟧ "semantic brackets" (double square brackets)
⟦a ∧ b⟧e "the truth value of a∧b in the environment e"
for example,
if e is a world such that e(a) = true
e(b) = true
then ⟦a ∧ b⟧e = true
if e' is a world where e(a) = false
e(b) = true
then ⟦a ∧ b⟧e' = false
Q: can we use another variable than v to avoid collision
with ∨ v ∨ v ∨
φ ⇒ ψ ≡ ¬φ ∨ ψ
φ ⇒ ψ ≡ ¬ψ ⇒ ¬φ
Q: What's the difference between → and ⇒
A: Its thickness.
For our purposes, literally nothing, I use
them interchangably.
⇛ means the same thing as ⊧
→ means the same thing as ⇒
φ ⇔ ψ ≡ (φ ⇒ ψ) ∧ (ψ ⇒ φ)
if e is a world such that e(a) = true
e(b) = true
⟦a ∧ b⟧e =
⟦a⟧e && ⟦b⟧e =
e(a) && e(b) =
true && true =
true
Example
a ∧ b is *satisfiable*
but not *valid*
a ∧ ¬a is *unsatisfiable*
a ∨ ¬a
is *satisfiable*
and *valid*
We use three different
notations for negation
¬a
a'
a with a bar
!a is boolean algebra complement
' gets used (confusingly)
both for complement
and negation
Q: what software do I use
to type in?
A: emacs with
major mode holscript-mode
In CNF:
conjunctions cannot appear
underneath disjunctions
in your syntax tree
disjunctions cannot appears
under negations
you can't double negation
(a ∨ b) ∧ (¬¬a ∨ c)
^ not CNF
We'll sometime write
pqr for p∧q∧r
Fun fact:
it's possible for a formula
to be *both* in CNF and DNF
a ∨ b is both in CNF and DNF
it's in CNF
because it's a unary
conjunction of a disjunction
it's in DNF
because it's a disjunction
of unary conjunctions
Q: can we think of ⊤ as empty
conjunction, and ⊥ as empty
disjunction in this def?
A: Yes
If we have a DNF formula:
(a ∧ b ∧ c) ∨
(a ∧ ¬a) ∨
(b ∧ c ∧ d)
the whole thing is satisfiable
if one disjunct is
(a ∨ b ∨ c) ∧
(a ∨ ¬a) ∧
(b ∨ c ∨ d)
Possible objection:
Why do we need this?
We already have a very
easy way of checking validity
and satisfiability:
draw a truth table!
Issue:
The size of your truth table
is 2^n, where n is the
number of values
The checks for CNF and DNF
are linear in the size of the
formula
¬(a ∧ b) ≡ (¬a) ∨ (¬b)
a ∧ (b ∨ c) ≡ (a ∧ b) ∨ (b ∧ c)
f(λ) = 0
f(a) = 0
f(abw) = 1 + f(bw)
Theorem bla:
f(w) ≤ length(w)
Proof
By structural induction on w
Base case: f(λ) ≤ length(λ)
(easy)
Inductive case:
assume (IH) f(w) ≤ length(w)
we need to show f(aw) ≤ length(aw)
By case analysis on w.
Case 1: w = λ
f(a) = 0 ≤ 1 = length(a)
Case 2: w = bw' for some b and w'
cheat
QED
Formal proofs have more utility in CS than pure mathematics
In pure mathematics: the objects you reason about
are purely theoretical constructs,
and aren't necessarily directly used in the world
Therefore: nobody cares is the individual steps in
your proof are wrong, or even if your
claim is technically wrong
as long as it would be easy to fix
In CS: if I'm proving the proposition
"my nuclear power plant control software
will never trigger the meltdown state"
Suddenly: it doesn't matter if it's "easy" to fix,
it matters if I actually did
At this point, people get confused.
If I have a proof ⊢ A ∧ B,
then I can invoke the ∧-elimination rule
to get a proof of ⊢ A
Why would you want to prove
something smaller from something bigger?
Inference rules are crafting recipes
(for proofs)
Q: What can you make with a
cobblestone and a stick?
A: Lever
We could write this crafting recipe
as an inference rule:
⊢ cobblestone ⊢ stick
_________________________
⊢ lever
Q: What do you get with 9 iron ingot?
A: Iron block
Q: What do you get with 1 iron block?
A: 9 iron ingots
Q: Why on earth would you want to
"downgrade" by making ingots
from your block?
A: Maybe you want to use another recipe
that requires ingots specifically
(e.g. maybe I want a pickaxe)
A ∧ B
_________ ∧-E1
A
A ∧ B
_________ ∧-E2
B
A B
_________ ∧-I
A ∧ B
With these inference rules, we could prove e.g.
A ∧ B ⊢ B ∧ A
To do that: find a way to string
together the rules that
end in the conclusion,
and start from the premise
A ∧ B A ∧ B
______∧-E2 _______ ∧-E1
B A
_________________ ∧-I
B ∧ A
^ now, we've built a tree,
where every step is justified by an inference rule
every leaf of the tree is A∧B (our assumption)
the root of the tree is B∧A (our desired conclusion)
Thus: we've done our first ND proof!
A ∧ B ⊢ B ∧ A
The calculus of natural deduction is
just a set of inference rules like the above.
Broadly speaking:
each connective has two kinds of inference rules
associated with it:
*introduction rules*
used when you want to prove a statement
where the connective is your outermost operator
A B
_____ ∧I
A ∧ B
*elimination rules*
used when the connective in question is
the outermost operator in a *premise*
A ∧ B
_____ ∧E-1
A
A
__________ ∨-I-1
A ∨ B
B
__________ ∨-I-2
A ∨ B
A ∧ B A ∧ F
______∧-E2 _______ ∧-E1
B A
_________________ ∧-I
B ∧ A
{A ∧ B, A ∧ F} ⊢ B ∧ A